COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	REHABILITATING FREGE
C00008 ENDMK
C⊗;
REHABILITATING FREGE


	Frege's original system of predicate logic allows any predicate
to be applied to any entity including other predicates with no types
whatsoever.  It appeals to the intuition, and it is simpler than any
other logical system.  Unfortunately, as Russell pointed out in time
for Frege to express his dismay in his book expounding the system,
it suffers from Russell's paradox.  In modern notation, the paradox
is obtained as follows:

Define the predicate ⊗hetero by

	%2∀x. hetero(x) ≡ ¬x(x)%1,

and substitue ⊗hetero for ⊗x getting

	%2hetero(hetero) ≡ ¬hetero(hetero)%1,

a contradiction.

	Subsequent systems of logic avoid the paradox by banning ⊗x(x) in
one way or another.  First order logic avoids predicates as arguments
entirely, higher order logic sets up a hierarchy up to some ordinal, and
set theory requires that all descending chains of set inclusion be finite.
All these devices are somewhat unnatural and lack some expressive power.
For example, one can define the notion of transitivity as follows:

	%2∀p. transitive(p) ≡ ∀x y z.(p(x,y)∧p(y,z) ⊃ p(x,z))%1.

This definition works fine in second order logic for defining the
transitivity of first order predicates, but second order predicates
can also be transitive.  Does one really need an infinite number of
definitions of transitivity when Frege required only one?  As I
understand it, Russell got out of this one, by allowing certain
formulas to be regarded as %2typically ambiguous%1.

	However, it seems that no matter how much you extend the
language in order to get in some new concept, there are additional
intuitively meaningful concepts that your extended language doesn't
cover.  %2I would like to conjecture that this is a mathematical
fact in the following sense:%1

	Suppose we use Frege's language as a basic language.  Formulas
like the definition of transitivity seem to be meaningful and formulas
like that involved in Russell's paradox seem unmeaningful.  What if
there is a definite notion of meaningfulness, but the set of
meaningful formulas is not recurseive or perhaps not even
recursively enumerable?  If this is true,
then any attempt to carve out the meaningful formulas by a decidable
criterion for well-formedness would fail.  A proof of this by some
diagonal argument might give for every recursively enumerable set
of meaningful formulas, a new formula that is meaningful but which
doesn't belong to the set.

	It is not immediately clear what is to be meant by meaningful,
but one approach would involve extending Dana Scott's work on models
for the λ-calculus to include quantifiers.  We could then say that
use the modelability of a set of predicate letters by partial functions
so that the set of formulas had defined truth values as a criterion
of meaningfulness.

Here are some ideas on what the logic might be like:

	We allow the usual propositional and predicate operators
and the propositional operator * with meaning "is defined".  Some
rules of inference are:

p,p⊃q => q; modus ponens

p,q	=> p∧q

p	=> p∨q
q	=> p∨q; these commit us to the commutative ∨.

*p	=> p∨¬p

*p	=> *¬p

(We will not include **p as a schema in contrast to (McCarthy 1964)).
Therefore, there are no tautologies.

There is more to come